This invention relates in general to model checking and, in particular, to model reduction techniques embedded in computer-implemented model checking.
xe2x80x94Ilan Beer, Shoham Ben-David, Avner Landverxe2x80x94xe2x80x9cOn-The-Fly Model Checking of RCTL Formulasxe2x80x9d, Computer Aided Verification, CAV ""98, LNCS 1427 Canada, 1998.
xe2x80x94Edmund M Clarke, Orna Grumberg, Doron Peledxe2x80x94xe2x80x9cModel Checkingxe2x80x9d, The MIT Press, Cambridge, Massachusetts London England, 1999 pp. 1-11.
xe2x80x94Hopcroft John E, Ullrnan Jeffrey Dxe2x80x94xe2x80x9cIntroduction to Automata Theory, Languages and Computationsxe2x80x9d, Addison Wesley, New York, 1979.
xe2x80x94Matt Kaufmann, Andrew Martin, Carl Pixleyxe2x80x94xe2x80x9cDesign Constraints in Symbolic Model Checkingxe2x80x9d, CAV ""98, LNCS 1427 Canada, 1998.
xe2x80x94Kenneth L. McMillanxe2x80x94xe2x80x9cSymbolic Model Checkingxe2x80x9d, Kluwer Academic Publishers, Massachusetts, 1993.
When designing systems that can be modeled as Finite State Machines, tools are used to check the correctness of the final design with respect to a design specification before proceeding to mass-production. A formal verfication tool is usually a computer program which requires as input a mathematical model of the system and a specification of desired design criteria. Thus, for example, in an integrated circuit including combinatorial gates and memory elements the circuit may generate an acknowledge signal (ACK) in response to a request signal (REQ) and the design specification may require that the REQ signal will be followed by the ACK signal within three clock cycles.
From a knowledge of the design specification and the mathematical model of the integrated circuit, a computer program can determine whether the model meets the specified design criteria. In the xe2x80x9ctemporal logic model checkingxe2x80x9d approach for formal verification, specifications are usually expressed in a propositional temporal logic, and circuit designs and protocols are modeled as state-transitions systems. An efficient search procedure is then used to determine if the specification holds on the state-transition system. In other words, a computer program checks whether the state-transition system is a model for the specification [CGP].
This approach suffers from the state-explosion problem. That is, the size of the state-space of the model is exponential in the number of its state-variables. Since the search procedure explores the state-space, its complexity is exponential in the number of state-variables as well. Thus the size of the designs which can be verified by model checking, using given computer resources such as memory and processing capacity, is severely limited.
Hence automated means to reduce the state-space are extremely important for making the technique of model checking tractable for industrial size designs.
A reduction is a procedure that reduces the state-space, while preserving anti-validity of the formula (i.e. if a propositional temporal logic formula is not valid in the reduced model it is also not valid in the original model). Naturally, the more the reduction can cut off the state-space, the better its merit will be. A natural way to reduce the state-space is to limit the behaviors of the environment. Since the model is comprised of the design under verification and its environment, reduction of the state space can be achieved by way of restricting the environment.
One traditionally used method for writing environment models is describing them via a Finite State Machine (FSM). Another way, used by Carl Pixley [KMP] is to specify environment models as a collection of Boolean constraints. In this approach, all inputs of the design under test are left free, but in the course of reachability analysis the model-checker discards all states that violate any of the user-specified Boolean constraints.
Other tools [FormalCheck(TM), CVE(TM)] enable the user to describe models via temporal constraints.
This invention introduces an innovative way to describe models (and in particular environment models), using regular expressions.
It is therefore straightforward that the user desires a reduction, which removes all paths that do not lead to any of the behaviors he aims at verifying. Intuitively, the user would wish to guide the search to error-prone areas of the design, while completely disregarding the rest. However, with the existing methods for model description, mainly by deployment of finite state machines (FSMs), the user might find it difficult to manipulate the model in such a manner so that scenarios of interest, and only scenarios of interest, occur.
Loosely speaking, it would be desirable to give the user the ability to describe, with minimum effort (specifically without the need for FSM implementation), a restricted model, in which the state-space includes only paths specified by her to be of interest. Such a reduced state space model would be amenable to analysis using a smaller memory than the complete state-space model and would be analyzed more quickly for a given computer processing capacity.
It is thus an object of the invention to restrict the computaion-tree to include only model behaviors described by the user (via the regular expression) as interesting.
This object is realized in accordance with a first aspect of the invention by a computer-implemented method for pruning a computation-tree defining a set of model behaviors of a state machine to a subset of the model behaviors, thereby reducing a size of the computation-tree and allowing analysis thereof by a computer in a shorter calculation time than would be possible for the complete computation-tree, said method comprising the steps of:
(a) obtaining as input:
i) a mathematical model of a Finite State Machine, and
ii) a Regular Expression defining a set of behaviors that are of interest to the user,
(b) using the Regular Expression to construct:
i) a finite automaton accepting all prefixes of words accepted by the Regular Expression, and
ii) a Boolean expression that realizes a property that the state is part of some path of a behavior defined by the Regular Expression, i.e. the expression evaluates to a first logic symbol for each of said words that are defined by the Regular Expression and evaluates to a second logic symbol otherwise, and
(c) exploring a state space of a product machine comprising the Finite State Machine and the constructed finite automaton such that for each state of the product machine there exists a corresponding Finite State Machine component and a corresponding finite automaton component, and for each explored state of the product machine, if the finite automaton component of a currently explored state of the product machine does not satisfy the Boolean Expression, then:
(d) pruning the currently explored state from the computation tree so as to abort further exploration from the currently explored state.
To achieve this goal, the user is required to declare the set of desired behaviors, by means of a regular expression. The restrict algorithm aims at removing all sub-trees of the computation-tree that correspond to undesired behaviors. This task requires the ability to identify when an execution path is one of the desired behaviorsxe2x80x94a task which is also embedded as part of the algorithm.
The restrict algorithm according to the invention offers what is believed to be an improved way of specifying modelsxe2x80x94by regular expressions, which constrain the paths to be considered by the model checker. This method is a generalization of the Boolean constraint method and can be used together with the FSM method. The generalization is due to the fact that while the Boolean constraints method discards xe2x80x98bad statesxe2x80x99, this method discards xe2x80x98bad finite computationsxe2x80x99.
Although conceptually the invention is associated with a computation-tree, what is actually manipulated is a finite state machine and its underlying state-space. Traversing this space induces a computation-tree, where each state that is reached constitutes a root of the sub-tree of all possible future continuations of this computation. The operation of pruning a sub-tree is implemented as omission of the state representing the root of this sub-tree. Thus, instead of realizing a mechanism that identifies paths corresponding to allowed behaviors, the invention implements a mechanism for identifying states (in the computation-tree) that are part of (at least) one of the desired behaviors.
The identification mechanism (constructed during the preprocessing stage) consists of a non-deterministic finite automaton (NFA), accepting the language of all prefixes of the regular expression, describing the desired behaviors. This NFA is denoted as a satellite. A path u is a prefix of a regular expression if it is in the language of the regular expression or if a path starting by u and followed by v is in the language of the regular expression. Hence, we can say that the accepting satellite-states capture the property until now, the execution did not xe2x80x98misbehavexe2x80x99 while the rejecting satellite-states capture the property the execution xe2x80x98misbehavedxe2x80x99.
In the processing stage, the states of a product machine comprising the Finite State Machine and the constructed NTA are explored. States of the product machine are comprised of two components, one corresponding to the Finite State Machine component and the other corresponding to the constructed NFA. When a state is explored, if the NFA component of the currently explored state of the product machine does not satisfy the Boolean Expression, then it is discarded by the search algorithm (as if it was not explored). The fact that the NFA component of the currently explored state does not satisfy the regular expression indicates that the Finite State Machine has rendered into a state that does not participate in any of the allowed behaviors (according to Regular Expression). Any state that can be explored from this state onwards, will not be a part of any of the allowed behaviors as well. Hence, ignoring the state (as if it was not explored) implements pruning from the computation tree a sub-tree whose root is the point in which the Finite State Machine xe2x80x9cmisbehavedxe2x80x9d, i.e. does not obey any of the allowed behaviors. This procedure results in a reduced state-space, representing a computation-tree containing all and only paths corresponding to allowed behaviors.